/*
 * $Id: JPFChecker.java 2233 2007-04-18 14:49:48Z kofron $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Pavel Parizek <parizek@nenya.ms.mff.cuni.cz>
 * 
 */
package org.objectweb.fractal.bpc.jpf;

import java.util.Map;
import java.util.HashMap;
import java.util.Set;
import java.util.HashSet;
import java.util.Iterator;

import gov.nasa.jpf.JPF;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.search.SearchListener;

import org.objectweb.fractal.api.Component;
import org.objectweb.fractal.api.Interface;
import org.objectweb.fractal.api.NoSuchInterfaceException;
import org.objectweb.fractal.api.type.InterfaceType;
import org.objectweb.fractal.api.control.ContentController;
import org.objectweb.fractal.util.Fractal;

import org.objectweb.fractal.bpc.EnvironmentController;
import org.objectweb.fractal.bpc.ProtocolController;
import org.objectweb.fractal.bpc.checker.JPFStaticChecker;
import org.objectweb.fractal.bpc.checker.DFSR.Options;

import cz.cuni.mff.envgen.EnvGen;
import cz.cuni.mff.envgen.EnvDescriptor;
import cz.cuni.mff.envgen.ProtocolTransformer;
import cz.cuni.mff.envgen.ProtocolTransformerImpl;
import cz.cuni.mff.envgen.CodeGenerator;
import cz.cuni.mff.envgen.CodeGeneratorImpl;


/**
 * Frontend to the Environment Generator and Java PathFinder.
 */
public class JPFChecker
{
    /**
     * Checks that all primitive components in the hierarchy starting from <tt>comp</tt> obey their frame protocols.
     *
     * @param comp A target component.
	 * @param tmpDir path to the directory for generated files, etc.
     * @return Result of the check.
     */
    public static boolean check(Component comp, String tmpDir) throws JPFCheckerException
    {
        ContentController compContentCtrl = null;
        
        // try to get the content controller of the target component
        try 
        {
            compContentCtrl = Fractal.getContentController(comp);
        } 
        catch (NoSuchInterfaceException exc) 
        {
            // the target component is primitive
            compContentCtrl = null;
        }
        
        if (compContentCtrl != null)
        {
            // target component is composite 
            // call the check method recursively on all subcomponents of the current component
            
			boolean totalResult = true;
			
            Component[] subComps = compContentCtrl.getFcSubComponents();
            for (int subIdx = 0; subIdx < subComps.length; subIdx++) 
            {
                Component subComp = subComps[subIdx];
                
                boolean res = check(subComp, tmpDir);
                
                if (!res) totalResult = false;
            }

			return totalResult;
        }
        else
        {
            // component is primitive, so we check it with JPF
            
            ProtocolController compProtoCtrl = null;
            try
            {
                compProtoCtrl = (ProtocolController) comp.getFcInterface("protocol-controller");
            }
            catch (NoSuchInterfaceException exc)
            {
                compProtoCtrl = null;
            }
            // the component has no protocol associated with it
            if ((compProtoCtrl == null) || (compProtoCtrl.getFcProtocol() == null)) return true;
            
            
            EnvironmentController compEnvCtrl = null;
            try
            {
                compEnvCtrl = (EnvironmentController) comp.getFcInterface("environment-controller");
            }
            catch (NoSuchInterfaceException exc)
            {
                compEnvCtrl = null;
            }
            // the component has no environment associated with it
            if ((compEnvCtrl == null) || (compEnvCtrl.getFcValueSetsClass() == null) || (compEnvCtrl.getFcValueSetsClass().length() == 0)) return true; 
            
            EnvDescriptor envDesc = new EnvDescriptor();
            
            // get the name of the target component
            envDesc.componentName = getComponentName(comp);
            
            if (envDesc.componentName == null) throw new JPFCheckerException("Component's name is null");
            
            
            // fill the envDesc object with data loaded from ADL
            
            Object compContent = null;
            try
            {
                compContent = comp.getFcInterface("/content");
            }
            catch (NoSuchInterfaceException ex)
            {
                compContent = null;
            }
            
            if (compContent == null) throw new JPFCheckerException("Component " + envDesc.componentName + " has no content class defined");
            
            envDesc.contentClass = compContent.getClass().getName();
                
            // map of names of server fractal interfaces to names of Java interfaces that implement them
            envDesc.serverItfs = new HashMap();
                            
            // map of names of client fractal interfaces to names of Java interfaces that implement them 
            envDesc.clientItfs = new HashMap();

            // fill envDesc.serverItfs and envDesc.clientItfs
            Object[] compItfs = comp.getFcInterfaces();
            for (int itfIdx = 0; itfIdx < compItfs.length; itfIdx++)
            {
                Interface itf = (Interface) compItfs[itfIdx];
                
                String itfName = itf.getFcItfName();
            
                boolean isCtrlItf = (itfName.startsWith("/") || itfName.equals("component") || itfName.endsWith("-controller"));

                if (!isCtrlItf) 
                {
                    boolean isClientItf = ((InterfaceType) itf.getFcItfType()).isFcClientItf();
	            
                    String itfSignature = ((InterfaceType) itf.getFcItfType()).getFcItfSignature();
                
                    if (isClientItf) envDesc.clientItfs.put(itfName, itfSignature);
                    else envDesc.serverItfs.put(itfName, itfSignature);
                }
            }


			// if available, use a protocol provided by the EnvironmentController as the specification of environment's behavior
            envDesc.protocolStr = compProtoCtrl.getFcProtocol();
			if ((compEnvCtrl.getFcProtocol() != null) && (compEnvCtrl.getFcProtocol().trim().length() > 0)) envDesc.protocolStr = compEnvCtrl.getFcProtocol();

			String frameProtocol = compProtoCtrl.getFcProtocol();
    
			// events are extracted from the protocol, not from the list of public methods of client and server interfaces, because there is usually no client or server interface for Token
			String[] frameEvents = null;
			try
			{
				frameEvents = JPFStaticChecker.getEvents(frameProtocol);
			}
			catch (Exception ex)
			{
				throw new JPFCheckerException("Error during extraction of event names from a frame protocol", ex);
			}

			/*
            // extract all event names from a list of public methods of all interfaces of the component
            Set frameEventSet = new HashSet();
            
            // process client interfaces
            Iterator clientItfIt = envDesc.clientItfs.entrySet().iterator();
            while (clientItfIt.hasNext())
            {
                Map.Entry clientItfEntry = (Map.Entry) clientItfIt.next();
                
                String itfName = (String) clientItfEntry.getKey();
                String itfClassName = (String) clientItfEntry.getValue();
                
                Class itfClass = null;
                try 
                {
                    itfClass = Class.forName(itfClassName);
                }
                catch (ClassNotFoundException ex) { itfClass = null; }
                
                if (itfClass != null)
                {
                    java.lang.reflect.Method[] itfMethods = itfClass.getDeclaredMethods();
                    for (int i = 0; i < itfMethods.length; i++) frameEventSet.add(itfName+"."+itfMethods[i].getName());
                }
            }
            
            // process server interfaces
            Iterator serverItfIt = envDesc.serverItfs.entrySet().iterator();
            while (serverItfIt.hasNext())
            {
                Map.Entry serverItfEntry = (Map.Entry) serverItfIt.next();
                
                String itfName = (String) serverItfEntry.getKey();
                String itfClassName = (String) serverItfEntry.getValue();
                
                Class itfClass = null;
                try
                {
                    itfClass = Class.forName(itfClassName);
                }
                catch (ClassNotFoundException ex) { itfClass = null; }
                
                if (itfClass != null)
                {
                    java.lang.reflect.Method[] itfMethods = itfClass.getDeclaredMethods();
                    for (int i = 0; i < itfMethods.length; i++) frameEventSet.add(itfName+"."+itfMethods[i].getName());
                }
            }
			
            String[] frameEvents = (String[]) frameEventSet.toArray(new String[frameEventSet.size()]);
			*/
			
         
            envDesc.valueSetsClass = compEnvCtrl.getFcValueSetsClass();
                
            envDesc.userStubCode = compEnvCtrl.getFcUserStubCode();
        
            envDesc.userDriversCode = new HashMap();
            if (compEnvCtrl.getFcUserDriversCode() != null)
            {
                envDesc.userDriversCode.putAll(compEnvCtrl.getFcUserDriversCode());
            }
        
            envDesc.targetDir = tmpDir;
        
        
            ProtocolTransformer pt = new ProtocolTransformerImpl();
            CodeGenerator cg = new CodeGeneratorImpl();
                
            EnvGen envGen = new EnvGen();
            envGen.bindFc("ProtocolTransformer", pt);
            envGen.bindFc("CodeGenerator", cg);
                
            String mainClassName = envGen.getMainClassName(envDesc.componentName);
                 
            Map itf2class = null;
        
            try
            {
                System.out.println("Checking component " + envDesc.componentName + " ...");

                itf2class = envGen.generateEnvironment(envDesc);


				// apply mappings of fractal interface name to stub implementation class name, which are defined in ADL
				if (compEnvCtrl.getFcItfStubs() != null)
	            {
    	            itf2class.putAll(compEnvCtrl.getFcItfStubs());
        	    }
                
                // compile generated environment classes
                String javaFileName = envDesc.targetDir + java.io.File.separator + mainClassName.replace('.', java.io.File.separatorChar) + ".java";
                String[] javacArgs = new String[]{"-d", envDesc.targetDir, "-sourcepath", envDesc.targetDir, javaFileName};
                if (com.sun.tools.javac.Main.compile(javacArgs) != 0) throw new JPFCheckerException("Failed to compile the environment classes");
                
                String outputFileName = envDesc.targetDir + java.io.File.separator + envDesc.componentName+"_Output.txt";
				
				String protocolStatsFileName = envDesc.targetDir + java.io.File.separator + envDesc.componentName+"_ProtoStats.html";
                
                boolean res = runJPF(mainClassName, frameProtocol, itf2class, envDesc.serverItfs.keySet(), frameEvents, true, outputFileName, protocolStatsFileName);
                
                System.out.println("Component " + envDesc.componentName + " ... " + (res ? "OK" : "ERROR") + " ("+outputFileName+")");
                
                return res;
            }
            catch (Throwable ex)
            {
                throw new JPFCheckerException(ex);
            }
        }
    }
    
    /**
     * Returns the component name. Uses its name controller to obtain the name. If the name is null or the
     * name controller is not present, computes the name.  
     * @param comp The component
     * @return Component name
     */
    private static String getComponentName(Component comp) 
    {
        String name;
        
        try 
        {
            name = Fractal.getNameController(comp).getFcName();
            
            if (name == null) name = comp.toString();
        } 
        catch (Exception exc) 
        {
            // The component does not have a name assigned, this isn't actually a problem. Just the eventuall error message won't be so nice.
            name = comp.toString();
        }
        
        return name;
    }

    /**
     * Load a file from classpath.
     * @return content of the file.
     */
  	private static String loadFileFromClasspath(String classpathFile)
	{
        if (classpathFile == null) return null;
        
        String content = null;
        
        try
        {
            java.io.InputStream is = ClassLoader.getSystemClassLoader().getResourceAsStream(classpathFile);
            java.io.BufferedReader in = new java.io.BufferedReader(new java.io.InputStreamReader(is));
            
            content = "";
            
            String line = in.readLine();
            while (line != null)
            {
                content += line;
                content += "\n";
                
                line = in.readLine();
            }
            
            in.close();
        }
        catch (Exception ex)
        {
            ex.printStackTrace();
            content = null;
        }
        
        return content;
	}

    
    /**
     * This method runs the Java PathFinder together with the BP checker.
     * @param testedClass name of the main class of the tested component.
     * @param protocol behavior protocol of the tested component.
     * @param itf2class map of names of interfaces to names of classes that implement them.
     * @param serverItfs list of names of fractal server interfaces of the tested component.
     * @param events list of events that the protocol checker must be notified of. It should contain events for all public methods of Java interfaces that correspond to fractal client and server interfaces of the target component.
	 * @param checkTraces turns on/off extension of states with event traces.
     * @param outputFileName name of file where to print detailed information (error traces, number of states, etc).
	* @param protocolStatsFileName name of file where to print statistics on protocol usage monitor
     * @return true when no error was found, false otherwise.
     */
    public static boolean runJPF(String testedClass, String protocol, Map itf2class, Set serverItfs, String[] events, boolean checkTraces, String outputFileName, String protocolStatsFileName) throws Exception
    {
        java.io.PrintStream errorOut = new java.io.PrintStream(new java.io.FileOutputStream(outputFileName));
        
        // System.out and System.err are redirected to our own errorOut because we want JPF to print its output to a file
        // JPF uses System.out and System.err quite extensively
        java.io.PrintStream origSystemOut = System.out;
        java.io.PrintStream origSystemErr = System.err;
        System.setOut(errorOut);
        System.setErr(errorOut);
        
        try
        {
            // checking with extension of state representation with event traces
            //String[] jpfArgs = new String[]{"+check.exectraces="+(checkTraces ? "true":"false"), testedClass};
            
            // checking with coordination of backtracking turned on
            String[] jpfArgs = new String[]{"+check.exectraces=false", "+search.class=org.objectweb.fractal.bpc.jpf.JPFCheckerSearch", "+jpf.report.publisher=gov.nasa.jpf.report.ConsolePublisher", "+jpf.report.console=jpf:result:trace:output:snapshot:statistics", "+jpf.report.console.show_cg=false", "+jpf.report.console.show_steps=true", "+jpf.report.console.show_location=true", "+jpf.report.console.show_source=true", "+jpf.report.console.show_method=false", "+jpf.report.console.show_code=false", testedClass};
				
            Config cfg = JPF.createConfig(jpfArgs);
                
            JPF jpf = new JPF(cfg);
                
            // second argument must be set to true if coordination of backtracking is to be used
            JPFStaticChecker checker = new JPFStaticChecker(protocol, true, errorOut);
    
            ProtocolListener pl = new ProtocolListener(checker.getNotifee(), itf2class, serverItfs, events);
            jpf.addSearchListener(pl);
			jpf.addVMListener(pl);
            jpf.addSearchProperty(pl);
            
            jpf.setProtocolMethods(pl.getMethodNames());
            
            ((JPFCheckerSearch) jpf.getSearch()).setJPFTraverser(checker.getNotifee());

			// turn on protocol usage monitor
			Options.monitorusage = true;
            
            jpf.run();
            
			// write protocol usage statistics
  			checker.writeUsageFile(new java.io.PrintStream(new java.io.FileOutputStream(protocolStatsFileName)));

			// turn off protocol usage monitor
			Options.monitorusage = false;

            return !jpf.foundErrors();
        }
        finally
        {
            // restore System.out and System.err
            System.setOut(origSystemOut);
            System.setErr(origSystemErr);
        }
    }

}
